Skip to content

introduce to_dstring #3110

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom
Merged
merged 1 commit into from
Feb 19, 2019
Merged

introduce to_dstring #3110

merged 1 commit into from
Feb 19, 2019

Conversation

kroening
Copy link
Member

@kroening kroening commented Oct 6, 2018 •
edited
Loading

As std::to_string, to_dstring produces a string from a number. A key
feature is that dstrings for values <=64 are pre-computed; generating
strings for such numbers is 50x faster than going via std::to_string.

int main()
{
  for(unsigned i=0; i<20000000; i++)
  {
    dstringt d;
    int j=20;
    d=dstringt(std::to_string(j));
  }
}

This is 2.5s as above, and 0.05s with to_dstring.

  • Each commit message has a non-empty body, explaining why the change was made.
  • My contribution is formatted in line with CODING_STANDARD.md.
  • Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
  • Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
  • My commit message includes data points confirming performance improvements (if claimed).
  • My PR is restricted to a single feature or bugfix.
  • White-space or formatting changes outside the feature-related changed lines are in commits of their own.

@kroening kroening requested review from smowton and tautschnig October 6, 2018 21:50
smowton
smowton reviewed Oct 7, 2018
View reviewed changes
tautschnig
tautschnig reviewed Oct 7, 2018
View reviewed changes
src/util/dstring.h Outdated
@@ -209,4 +209,21 @@ struct diagnostics_helpert<dstringt>
}
};

#define DSTRING_NUMBERS_MAX 64
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Why is 64 the optimal number (also, this define should go in util/magic.h)?

@smowton
Copy link
Contributor

smowton commented Oct 8, 2018

Looks like the CI culprit is dstringt == std::string rather than clang?

tautschnig
tautschnig requested changes Oct 8, 2018
View reviewed changes
Copy link
Collaborator

@tautschnig tautschnig left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Marking this as request-changes until the magic-number question is resolved.

allredj
allredj reviewed Oct 8, 2018
View reviewed changes
Copy link
Contributor

@allredj allredj left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This PR failed Diffblue compatibility checks (cbmc commit: 63d1a57).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/87195826
Status will be re-evaluated on next push.
Please contact @peterschrammel, @thk123, or @allredj for support.

Common spurious failures:

  • the cbmc commit has disappeared in the mean time (e.g. in a force-push)
  • the author is not in the list of contributors (e.g. first-time contributors).

allredj
allredj reviewed Oct 14, 2018
View reviewed changes
Copy link
Contributor

@allredj allredj left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Passed Diffblue compatibility checks (cbmc commit: 65891d2).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/87883391

@tautschnig tautschnig assigned kroening and unassigned smowton and tautschnig Oct 18, 2018
@kroening kroening assigned tautschnig and unassigned kroening Feb 17, 2019
tautschnig
tautschnig reviewed Feb 17, 2019
View reviewed changes
Copy link
Collaborator

@tautschnig tautschnig left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'll include it in my profiling, will report back.

src/util/magic.h
@@ -13,4 +13,7 @@ const std::size_t STRING_REFINEMENT_MAX_CHAR_WIDTH = 16;
// Limit the size of strings in traces to 64M chars to avoid memout
const std::size_t MAX_CONCRETE_STRING_SIZE = 1 << 26;

// The top end of the range of integers for which dstrings are precomputed
constexpr std::size_t DSTRING_NUMBERS_MAX = 64;
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Is there any value in using constexpr over const?

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@kroening ?

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Only that you can then could produce constexpr dstrings for numbers up to that value from a constexpr integer.

tautschnig
tautschnig reviewed Feb 17, 2019
View reviewed changes
introduce to_dstring
e3f19d2 
As std::to_string, to_dstring produces a string from a number.  A key
feature is that dstrings for values <=64 are pre-computed; generating
strings for such numbers is 50x faster than going via std::to_string.

int main()
{
  for(unsigned i=0; i<20000000; i++)
  {
    dstringt d;
    int j=20;
    d=dstringt(std::to_string(j));
  }
}

This is 2.5s as above, and 0.05s with to_dstring.
allredj
allredj reviewed Feb 17, 2019
View reviewed changes
Copy link
Contributor

@allredj allredj left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

✔️
Passed Diffblue compatibility checks (cbmc commit: e3f19d2).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/101224713

tautschnig
tautschnig approved these changes Feb 17, 2019
View reviewed changes
Copy link
Collaborator

@tautschnig tautschnig left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

On ReachSafety-ControlFlow this optimisation reduces the number of string-table lookups from 62778903 to 27037069 (and the time spent in irept::set(dstringt const&, long long) from 22.52 seconds to 13.58 seconds).

@tautschnig tautschnig assigned kroening and unassigned tautschnig Feb 17, 2019
@kroening
Copy link
Member Author

Many thanks for the benchmarking -- I should really set up some set of benchmarks for this purpose!

@tautschnig tautschnig merged commit d683a70 into develop Feb 19, 2019
@tautschnig tautschnig deleted the to_dstring branch February 19, 2019 00:42
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@allredj allredj allredj left review comments

@smowton smowton smowton approved these changes

@tautschnig tautschnig tautschnig approved these changes

@peterschrammel peterschrammel Awaiting requested review from peterschrammel peterschrammel is a code owner

@pkesseli pkesseli Awaiting requested review from pkesseli

Assignees

@kroening kroening

Labels
enhancement
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
4 participants
@kroening @smowton @tautschnig @allredj